package ch.epfl.lara.matcheck.verify;


import ch.epfl.lara.matcheck.ast._
import ch.epfl.lara.matcheck.verify.provers.ProverResults
import ch.epfl.lara.matcheck.verify.spec._
import ch.epfl.lara.matcheck.verify.spec.exceptions.DomainDeclarationEmpty

import scala.util.parsing.input.Position

class Verify extends VerifyMatch {
  
  private var matchPos: (Position,Boolean) = (null,false)
  
  
  def this(program: Program) = {
    this()
    
    Timer.startSpecVerification()
    verifySpec(program)
    Timer.finishedSpecVerification()
    
    val vprogram = TransformProgram(program)
    verifyMatches(vprogram)
  }
  
  
  def verifySpec(program: Program) {
      if(!Config.NOSPEC) {
        Report.verbose("====================================================")
        Report.verbose("=== Starting program's specification verification ==")
        Report.verbose("====================================================\n")
        try {
          
          Report.verbose("\n1. Verifying extractors' domain declaration ...")
          Report.verbose("-------------------------------------------------\n")
          
          Timer.startDomainVerification()
          new DomainSpecVerifier(program.domain,program.objects)
          Timer.finishedDomainVerification()
          
          
        } catch {
          case d : DomainDeclarationEmpty => Timer.finishedDomainVerification() // good
        }
        Report.verbose("\n2. Verifing methods' specification ...")
        Report.verbose("----------------------------------------\n")
        new ProgramSpecVerifier(program)
        
        
      }
  }
  
  
  def verifyMatches(vprogram: VProgram) {
    Report.verbose("\n====================================================")
    Report.verbose("========= Starting Pattern Matching Analysis =========")
    Report.verbose("====================================================\n\n")
    
    for(vm @ VMatch(scrut,cases) <- CollectVMatches(vprogram)) {
      val pFormulas = cases.map(_.formula)
      matchPos = (vm.pos,false)
      check(And(AxiomsHolder.axioms,scrut),pFormulas)
    }
  }
  
  
  
  
  private def check(axiom: Axiom, pFormulas: List[Imply]) {
    if(Config.COMPLETE)  checkComplete(axiom,pFormulas)
    if(Config.DISJOINT)  checkDisjoint(axiom,pFormulas)
    if(Config.REACHABLE) checkUnreachable(axiom,pFormulas)
  }
  
  
  private def checkAndtime(formula: Formula) = {
    Timer.startPmProver()
     val result = Config.PROVER(formula)
    Timer.finishedPmProver()
    result
  }
  
  
  private def checkComplete(axiom: Axiom, pFormulas: List[Imply]) {
    val complete_formula = complete(axiom,pFormulas)
    
    checkAndPromptVerbose_?("Checking completeness ... ", complete_formula)
    
    debugFormula(complete_formula)
  }
  
  
  private def checkAndPromptVerbose_?(msg: String, formula: Formula) {
    var verbose = Config.VERBOSE || Config.DEBUG
    val(pos,prompted) = matchPos
    def promptLineAndMsg {
      if(verbose) {
        if(!prompted) {
          Report.println(pos)
          matchPos = (pos,true)
        }
        Report.print(msg)
      }
    }
    
    promptLineAndMsg
    
    val result = checkAndtime(formula)
    
    result match {
      case ProverResults.Valid => ()
      case _ if !verbose => 
        verbose = true
        promptLineAndMsg
      case _ => ()
    }
    
    if(verbose) Report.println(result.toString)
    
  }
  
  
  protected def checkDisjoint(axiom: Formula, pFormulas: List[Imply]) {
    val disjoint_formula = disjoint(axiom,pFormulas)
    
    checkAndPromptVerbose_?("Checking disjointness ... ", disjoint_formula)
    
    debugFormula(disjoint_formula)
  }
  
  
  
  
  protected def checkUnreachable(axiom: Axiom, pFormulas: List[Imply]) {    
    var result: ProverResults.ProverResult = ProverResults.Valid
    var continue = true
    var timeout = false
    
    if(Config.VERBOSE || Config.DEBUG) {
      val(pos,prompted) = matchPos
      if(!prompted) {
        Report.println(pos)
        matchPos = (pos,true)
      }
      Report.print("Checking reachability ... ")
    }
    
    val unreachable_formula = unreachable(axiom,pFormulas)
    for(formula <- unreachable_formula) {
      if(continue){
      checkAndtime(formula) match {
        case ProverResults.Valid   => 
          result = ProverResults.Invalid
          continue = false
          
        case ProverResults.Timeout => 
          result = ProverResults.Timeout
          timeout = true
          
        case ProverResults.Invalid =>  
      }
      }
    }
    
    if(Config.VERBOSE || Config.DEBUG) {
      Report.println(result.toString)
    } else if(!continue || timeout) {
      val(pos,prompted) = matchPos
      if(!prompted) {
        Report.println(pos)
        matchPos = (pos,true)
      }
      Report.println("Checking reachability ... " + result.toString)
    }
    debugFormula(unreachable_formula)
   
  }
  
  
  
  
  
  private object CollectVMatches {
    
    def apply(vtrees: List[VTree]): Stream[VMatch] = 
      vtrees.toStream.flatMap(this(_))
    
    def apply(vtree: VTree): Stream[VMatch] = vtree match {
      case VProgram(_,conts) => this(conts)
      case VContainer(_,methods)  => this(methods)
      case VMethodDef(_,_,body)   => this(body)
      case VIf(cond,then,elze)    => Stream.concat(this(then),this(elze))
      case vm @ VMatch(_,cases)   => Stream.cons(vm,this(cases.map(_.body)))
      case VSimpleExpr            => Stream.empty
    }
  }
  
  
  
  private def debugFormula(f: Formula) {
    Report.debug("\n"+Config.PROVER.asString(f)+"\n")
  }
  
  
  
  private def debugFormula(fs: List[Formula]) {
    fs.foreach(debugFormula(_))
  }
  
}
